Inference at * 
Iof proof for Lemma sq stable inv funs:


  A, B:Type, f:(AB), g:(BA). SqStable(InvFuns(A;B;f;g)) 

latex

 by ((((((Unfold `inv_funs` 0) 
CollapseTHEN (UnivCD))) 
CollapseTHENM (ProveSqStable))) 

CoCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
C) inil_term))) 

latex

C.

Definitions	t  T, , InvFuns(A;B;f;g), x:A. B(x), P  Q
Lemmas	sq stable equal, tidentity wf, compose wf, sq stable and